Storm 1.5.1
Date: Tue Apr 28 12:23:28 2020
Command line arguments: --prism nand.prism --prop nand.props reliable --constants 'N=40,K=4' --exact --ddlib sylvan '--sylvan:maxmem' 6114 '--sylvan:threads' 4
Current working directory: /
Time for model input parsing: 0.003s.
Time for model construction: 37.991s.
--------------------------------------------------------------
Model type: DTMC (sparse)
States: 3999522
Transitions: 6288542
Reward Models: none
State Labels: 3 labels
* deadlock -> 0 item(s)
* ((s = 4) & ((z / 40) < 1/10)) -> 4 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "reliable": P=? [F ((s = 4) & ((z / 40) < 1/10))] ...
Result (for initial states): 7073410276867630182036256400888394636401281117838496193329308323687125707403234304583554599059642891015434709050290014659339126304802694362252183431807177003633968280617618995071337263400451170114626733996748290675371799715662983419506318701718558795860406494115162261649890650251693555717374614594670943847433539070343259606254316245084716000896473482539769578265846578050874211797180613965882452295534277381831975275853494748435478879461635997848648515103809170427736893067597368369125722353133284605839381110231288435557905276235846112930375580391379431641001473203640322244029437131656432754007785810519373450767717313409320241381606121889757/11433026582770433444150841434946575983665790023011997239866893501124069401225141786043274075451132615716021287640033707692804831240670294973965820412638988355604337906057133982774690808247500425599746811586452854879494120350499663410752853418655568298801018707370085780279622235281919773885153915410742665432027264385939603794342761535883881589330478746513396975860783173588783333310428610837885469575737992226585096003257861714861056977505239452452401210690205384130399418976115047153237702913577842484321014952056001690525414886369612166053431447977273573548482850717467051993025961564853787422180175781250000000000000000000000000000000000000000 (approx. 0.6186822208)
Time for model checking: 46.594s.